The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^1)).

0 CpxTRS
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CdtProblem
    ↳3 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳4 CdtProblem
    ↳5 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳6 CdtProblem
    ↳7 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳8 CdtProblem
    ↳9 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳10 CdtProblem
    ↳11 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳12 CdtProblem
↳13 CpxTrsMatchBoundsTAProof (⇔, 17 ms)
↳14 BOUNDS(O(1), O(n^1))

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

p(p(b(a(x0)), x1), p(x2, x3)) → p(p(b(x2), a(a(b(x1)))), p(x3, x0))

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

p(p(b(a(z0)), z1), p(z2, z3)) → p(p(b(z2), a(a(b(z1)))), p(z3, z0))
Tuples:

P(p(b(a(z0)), z1), p(z2, z3)) → c(P(p(b(z2), a(a(b(z1)))), p(z3, z0)), P(b(z2), a(a(b(z1)))), P(z3, z0))
S tuples:

P(p(b(a(z0)), z1), p(z2, z3)) → c(P(p(b(z2), a(a(b(z1)))), p(z3, z0)), P(b(z2), a(a(b(z1)))), P(z3, z0))
K tuples:none
Defined Rule Symbols:

p

Defined Pair Symbols:

P

Compound Symbols:

c

(3) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace P(p(b(a(z0)), z1), p(z2, z3)) → c(P(p(b(z2), a(a(b(z1)))), p(z3, z0)), P(b(z2), a(a(b(z1)))), P(z3, z0)) by

P(p(b(a(x0)), x1), p(x2, x3)) → c(P(p(b(x2), a(a(b(x1)))), p(x3, x0)), P(x3, x0))

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

p(p(b(a(z0)), z1), p(z2, z3)) → p(p(b(z2), a(a(b(z1)))), p(z3, z0))
Tuples:

P(p(b(a(x0)), x1), p(x2, x3)) → c(P(p(b(x2), a(a(b(x1)))), p(x3, x0)), P(x3, x0))
S tuples:

P(p(b(a(x0)), x1), p(x2, x3)) → c(P(p(b(x2), a(a(b(x1)))), p(x3, x0)), P(x3, x0))
K tuples:none
Defined Rule Symbols:

p

Defined Pair Symbols:

P

Compound Symbols:

c

(5) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace P(p(b(a(x0)), x1), p(x2, x3)) → c(P(p(b(x2), a(a(b(x1)))), p(x3, x0)), P(x3, x0)) by

P(p(b(a(z0)), z1), p(a(y0), z3)) → c(P(p(b(a(y0)), a(a(b(z1)))), p(z3, z0)), P(z3, z0))
P(p(b(a(p(y2, y3))), z1), p(z2, p(b(a(y0)), y1))) → c(P(p(b(z2), a(a(b(z1)))), p(p(b(a(y0)), y1), p(y2, y3))), P(p(b(a(y0)), y1), p(y2, y3)))

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

p(p(b(a(z0)), z1), p(z2, z3)) → p(p(b(z2), a(a(b(z1)))), p(z3, z0))
Tuples:

P(p(b(a(z0)), z1), p(a(y0), z3)) → c(P(p(b(a(y0)), a(a(b(z1)))), p(z3, z0)), P(z3, z0))
P(p(b(a(p(y2, y3))), z1), p(z2, p(b(a(y0)), y1))) → c(P(p(b(z2), a(a(b(z1)))), p(p(b(a(y0)), y1), p(y2, y3))), P(p(b(a(y0)), y1), p(y2, y3)))
S tuples:

P(p(b(a(z0)), z1), p(a(y0), z3)) → c(P(p(b(a(y0)), a(a(b(z1)))), p(z3, z0)), P(z3, z0))
P(p(b(a(p(y2, y3))), z1), p(z2, p(b(a(y0)), y1))) → c(P(p(b(z2), a(a(b(z1)))), p(p(b(a(y0)), y1), p(y2, y3))), P(p(b(a(y0)), y1), p(y2, y3)))
K tuples:none
Defined Rule Symbols:

p

Defined Pair Symbols:

P

Compound Symbols:

c

(7) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace P(p(b(a(p(y2, y3))), z1), p(z2, p(b(a(y0)), y1))) → c(P(p(b(z2), a(a(b(z1)))), p(p(b(a(y0)), y1), p(y2, y3))), P(p(b(a(y0)), y1), p(y2, y3))) by

P(p(b(a(p(z2, z3))), x2), p(x3, p(b(a(z0)), z1))) → c(P(p(b(x3), a(a(b(x2)))), p(p(b(z2), a(a(b(z1)))), p(z3, z0))), P(p(b(a(z0)), z1), p(z2, z3)))
P(p(b(a(p(x0, x1))), x2), p(x3, p(b(a(x4)), x5))) → c

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

p(p(b(a(z0)), z1), p(z2, z3)) → p(p(b(z2), a(a(b(z1)))), p(z3, z0))
Tuples:

P(p(b(a(z0)), z1), p(a(y0), z3)) → c(P(p(b(a(y0)), a(a(b(z1)))), p(z3, z0)), P(z3, z0))
P(p(b(a(p(z2, z3))), x2), p(x3, p(b(a(z0)), z1))) → c(P(p(b(x3), a(a(b(x2)))), p(p(b(z2), a(a(b(z1)))), p(z3, z0))), P(p(b(a(z0)), z1), p(z2, z3)))
P(p(b(a(p(x0, x1))), x2), p(x3, p(b(a(x4)), x5))) → c
S tuples:

P(p(b(a(z0)), z1), p(a(y0), z3)) → c(P(p(b(a(y0)), a(a(b(z1)))), p(z3, z0)), P(z3, z0))
P(p(b(a(p(z2, z3))), x2), p(x3, p(b(a(z0)), z1))) → c(P(p(b(x3), a(a(b(x2)))), p(p(b(z2), a(a(b(z1)))), p(z3, z0))), P(p(b(a(z0)), z1), p(z2, z3)))
P(p(b(a(p(x0, x1))), x2), p(x3, p(b(a(x4)), x5))) → c
K tuples:none
Defined Rule Symbols:

p

Defined Pair Symbols:

P

Compound Symbols:

c, c

(9) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

P(p(b(a(p(x0, x1))), x2), p(x3, p(b(a(x4)), x5))) → c

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

p(p(b(a(z0)), z1), p(z2, z3)) → p(p(b(z2), a(a(b(z1)))), p(z3, z0))
Tuples:

P(p(b(a(z0)), z1), p(a(y0), z3)) → c(P(p(b(a(y0)), a(a(b(z1)))), p(z3, z0)), P(z3, z0))
P(p(b(a(p(z2, z3))), x2), p(x3, p(b(a(z0)), z1))) → c(P(p(b(x3), a(a(b(x2)))), p(p(b(z2), a(a(b(z1)))), p(z3, z0))), P(p(b(a(z0)), z1), p(z2, z3)))
S tuples:

P(p(b(a(z0)), z1), p(a(y0), z3)) → c(P(p(b(a(y0)), a(a(b(z1)))), p(z3, z0)), P(z3, z0))
P(p(b(a(p(z2, z3))), x2), p(x3, p(b(a(z0)), z1))) → c(P(p(b(x3), a(a(b(x2)))), p(p(b(z2), a(a(b(z1)))), p(z3, z0))), P(p(b(a(z0)), z1), p(z2, z3)))
K tuples:none
Defined Rule Symbols:

p

Defined Pair Symbols:

P

Compound Symbols:

c

(11) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace P(p(b(a(p(z2, z3))), x2), p(x3, p(b(a(z0)), z1))) → c(P(p(b(x3), a(a(b(x2)))), p(p(b(z2), a(a(b(z1)))), p(z3, z0))), P(p(b(a(z0)), z1), p(z2, z3))) by

P(p(b(a(p(a(y2), z1))), z2), p(z3, p(b(a(z4)), z5))) → c(P(p(b(z3), a(a(b(z2)))), p(p(b(a(y2)), a(a(b(z5)))), p(z1, z4))), P(p(b(a(z4)), z5), p(a(y2), z1)))
P(p(b(a(p(z0, z1))), z2), p(a(y2), p(b(a(z4)), z5))) → c(P(p(b(a(y2)), a(a(b(z2)))), p(p(b(z0), a(a(b(z5)))), p(z1, z4))), P(p(b(a(z4)), z5), p(z0, z1)))
P(p(b(a(p(z0, p(b(a(y4)), y5)))), z2), p(z3, p(b(a(p(y0, y1))), z5))) → c(P(p(b(z3), a(a(b(z2)))), p(p(b(z0), a(a(b(z5)))), p(p(b(a(y4)), y5), p(y0, y1)))), P(p(b(a(p(y0, y1))), z5), p(z0, p(b(a(y4)), y5))))

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

p(p(b(a(z0)), z1), p(z2, z3)) → p(p(b(z2), a(a(b(z1)))), p(z3, z0))
Tuples:

P(p(b(a(z0)), z1), p(a(y0), z3)) → c(P(p(b(a(y0)), a(a(b(z1)))), p(z3, z0)), P(z3, z0))
P(p(b(a(p(a(y2), z1))), z2), p(z3, p(b(a(z4)), z5))) → c(P(p(b(z3), a(a(b(z2)))), p(p(b(a(y2)), a(a(b(z5)))), p(z1, z4))), P(p(b(a(z4)), z5), p(a(y2), z1)))
P(p(b(a(p(z0, z1))), z2), p(a(y2), p(b(a(z4)), z5))) → c(P(p(b(a(y2)), a(a(b(z2)))), p(p(b(z0), a(a(b(z5)))), p(z1, z4))), P(p(b(a(z4)), z5), p(z0, z1)))
P(p(b(a(p(z0, p(b(a(y4)), y5)))), z2), p(z3, p(b(a(p(y0, y1))), z5))) → c(P(p(b(z3), a(a(b(z2)))), p(p(b(z0), a(a(b(z5)))), p(p(b(a(y4)), y5), p(y0, y1)))), P(p(b(a(p(y0, y1))), z5), p(z0, p(b(a(y4)), y5))))
S tuples:

P(p(b(a(z0)), z1), p(a(y0), z3)) → c(P(p(b(a(y0)), a(a(b(z1)))), p(z3, z0)), P(z3, z0))
P(p(b(a(p(a(y2), z1))), z2), p(z3, p(b(a(z4)), z5))) → c(P(p(b(z3), a(a(b(z2)))), p(p(b(a(y2)), a(a(b(z5)))), p(z1, z4))), P(p(b(a(z4)), z5), p(a(y2), z1)))
P(p(b(a(p(z0, z1))), z2), p(a(y2), p(b(a(z4)), z5))) → c(P(p(b(a(y2)), a(a(b(z2)))), p(p(b(z0), a(a(b(z5)))), p(z1, z4))), P(p(b(a(z4)), z5), p(z0, z1)))
P(p(b(a(p(z0, p(b(a(y4)), y5)))), z2), p(z3, p(b(a(p(y0, y1))), z5))) → c(P(p(b(z3), a(a(b(z2)))), p(p(b(z0), a(a(b(z5)))), p(p(b(a(y4)), y5), p(y0, y1)))), P(p(b(a(p(y0, y1))), z5), p(z0, p(b(a(y4)), y5))))
K tuples:none
Defined Rule Symbols:

p

Defined Pair Symbols:

P

Compound Symbols:

c

(13) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)

A linear upper bound on the runtime complexity of the TRS R could be shown with a Match-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 0.

The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by:
final states : [1]
transitions:
b0(0) → 0
a0(0) → 0
p0(0, 0) → 1

(14) BOUNDS(O(1), O(n^1))